T:Type, P:(T), L:(T List).
(0 < ||L||)
 (x, y:T. Dec(x = y))
 ((xL. yL. ((x = y  T))  (P(x)  P(y)))  (xL.yL. ((x = y  T))  P(y))) 

latex

Definitions	x:A. B(x), , P  Q, ||as||, P  Q, A, P  Q, x(s), Y, P & Q, P  Q, False, t  T, x. t(x), xL. P(x), {T}, (xL.P(x)), x:A. B(x), l[i], {i..j}, i  j < k, hd(l), nth_tl(n;as), if b then t else f fi , i z j, b, i <z j, tt, ff, Dec(P)
Lemmas	l all wf2, not wf, l member wf, l exists wf, decidable wf, implies functionality wrt iff, iff wf, iff functionality wrt iff, l exists cons, member wf, iff transitivity, l all cons, and functionality wrt iff, or functionality wrt iff, false wf, l exists nil, l all nil, length wf1, non neg length, cons member, select member, le wf